Namespace STACK_SIZE by willieyz · Pull Request #1396 · pq-code-package/mlkem-native

willieyz · 2025-12-16T05:53:35Z

Resolves: Namespace STACK_SIZE in various assembly files #1395
Assembly files may define local macros (e.g. STACK_SIZE, KECCAK_F1600_ROUNDS) without the MLK_ prefix, risking name clashes with symbols in consuming libraries.
To be consistent with the rest of the codebase, all such macros are prefixed with MLK_, bringing them in line with the established namespacing convention.

hanno-becker · 2025-12-17T04:13:16Z


-#define STACK_SIZE (16*6 + 8*8 + 6*8 + (STACK_LOCS) * 8)
+#define MLK_STACK_SIZE (16*6 + 8*8 + 6*8 + (STACK_LOCS) * 8)
 #define STACK_BASE_GPRS (6*8)


We shouldn't namespace STACK_SIZE, but not the other macros; either all of them, or none.

hanno-becker

If we do this we should namespace all macros in the assembly files.

Note that the lack of namespacing here is of little effect since all affected files are in dev/ and not in the main source tree.

oqs-bot · 2026-01-23T02:55:03Z

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1275s	1251s	+1.9%
`mlk_indcpa_keypair_derand`	✅	243s	244s	-0%
`mlk_indcpa_enc`	✅	164s	165s	-1%
`mlk_rej_uniform_c`	✅	112s	117s	-4%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	51s	47s	+9%
`mlk_ntt_layer`	✅	32s	27s	+19%
`mlk_poly_rej_uniform`	✅	29s	28s	+4%
`mlk_keccak_squeezeblocks_x4`	✅	27s	23s	+17%
`poly_ntt_native`	✅	26s	25s	+4%
`mlk_poly_reduce_native`	✅	20s	20s	+0%
`keccakf1600x4_permute_native_x4`	✅	18s	18s	+0%
`mlk_fqmul`	✅	15s	16s	-6%
`mlk_poly_decompress_d4_native`	✅	15s	12s	+25%
`mlk_polyvec_add`	✅	15s	11s	+36%
`mlk_indcpa_dec`	✅	13s	15s	-13%
`mlk_poly_decompress_d10_native`	✅	13s	12s	+8%
`mlk_keccak_squeezeblocks`	✅	9s	10s	-10%
`mlk_keccak_squeeze_once`	✅	8s	8s	+0%
`mlk_ntt_butterfly_block`	✅	8s	8s	+0%
`mlk_poly_frombytes_native`	✅	8s	8s	+0%
`mlk_poly_frommsg`	✅	8s	8s	+0%
`mlk_poly_cbd_eta2`	✅	7s	6s	+17%
`mlk_poly_ntt`	✅	7s	7s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	✅	7s	7s	+0%
`mlk_invntt_layer`	✅	6s	4s	+50%
`mlk_poly_rej_uniform_x4`	✅	6s	7s	-14%
`mlk_polyvec_ntt`	✅	6s	2s	+200%
`kem_check_pk`	✅	5s	4s	+25%
`mlk_poly_compress_d10_native`	✅	5s	1s	+400%
`mlk_poly_ntt_c`	✅	5s	3s	+67%
`mlk_scalar_compress_d5`	✅	5s	2s	+150%
`mlk_shake256x4`	✅	5s	3s	+67%
`poly_decompress_d4_native_x86_64`	✅	5s	4s	+25%
`poly_mulcache_compute_native_aarch64`	✅	5s	3s	+67%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	5s	6s	-17%
`rej_uniform_native_x86_64`	✅	5s	6s	-17%
`intt_native_aarch64`	✅	4s	2s	+100%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	4s	1s	+300%
`kem_dec`	✅	4s	3s	+33%
`kem_enc_derand`	✅	4s	3s	+33%
`mlk_keccak_absorb_once_x4`	✅	4s	6s	-33%
`mlk_keccakf1600_permute`	✅	4s	2s	+100%
`mlk_keccakf1600_permute_c`	✅	4s	5s	-20%
`mlk_keccakf1600x4_extract_bytes_c`	✅	4s	5s	-20%
`mlk_poly_cbd_eta1`	✅	4s	2s	+100%
`mlk_poly_compress_d5_c`	✅	4s	1s	+300%
`mlk_poly_decompress_d5_native`	✅	4s	2s	+100%
`mlk_poly_mulcache_compute_c`	✅	4s	3s	+33%
`mlk_poly_reduce_c`	✅	4s	2s	+100%
`mlk_poly_tomont_c`	✅	4s	1s	+300%
`mlk_polymat_permute_bitrev_to_custom`	✅	4s	1s	+300%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	4s	4s	+0%
`mlk_scalar_decompress_d10`	✅	4s	4s	+0%
`ntt_native_aarch64`	✅	4s	2s	+100%
`nttunpack_native_x86_64`	✅	4s	6s	-33%
`poly_frombytes_native_x86_64`	✅	4s	5s	-20%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	4s	4s	+0%
`rej_uniform_native`	✅	4s	4s	+0%
`keccakf1600_permute_native`	✅	3s	2s	+50%
`kem_check_sk`	✅	3s	2s	+50%
`kem_keypair`	✅	3s	4s	-25%
`mlk_ct_cmask_nonzero_u16`	✅	3s	1s	+200%
`mlk_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mlk_ct_sel_int16`	✅	3s	3s	+0%
`mlk_gen_matrix_serial`	✅	3s	3s	+0%
`mlk_keccak_absorb_once`	✅	3s	2s	+50%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	3s	1s	+200%
`mlk_poly_compress_d10`	✅	3s	3s	+0%
`mlk_poly_compress_d10_c`	✅	3s	2s	+50%
`mlk_poly_compress_d11`	✅	3s	3s	+0%
`mlk_poly_compress_d4_c`	✅	3s	3s	+0%
`mlk_poly_compress_dv`	✅	3s	2s	+50%
`mlk_poly_decompress_dv`	✅	3s	4s	-25%
`mlk_poly_getnoise_eta1_4x`	✅	3s	2s	+50%
`mlk_poly_mulcache_compute_native`	✅	3s	3s	+0%
`mlk_poly_tomont`	✅	3s	1s	+200%
`mlk_poly_tomont_native`	✅	3s	1s	+200%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	3s	2s	+50%
`mlk_polyvec_decompress_du`	✅	3s	2s	+50%
`mlk_polyvec_mulcache_compute`	✅	3s	1s	+200%
`mlk_polyvec_permute_bitrev_to_custom`	✅	3s	2s	+50%
`mlk_polyvec_tomont`	✅	3s	3s	+0%
`mlk_scalar_compress_d4`	✅	3s	2s	+50%
`mlk_scalar_decompress_d11`	✅	3s	1s	+200%
`mlk_shake128x4_absorb_once`	✅	3s	2s	+50%
`poly_decompress_d10_native_x86_64`	✅	3s	5s	-40%
`poly_invntt_tomont_native`	✅	3s	2s	+50%
`poly_mulcache_compute_native_x86_64`	✅	3s	2s	+50%
`poly_reduce_native_x86_64`	✅	3s	3s	+0%
`poly_tobytes_native_aarch64`	✅	3s	2s	+50%
`rej_uniform_native_aarch64`	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	1s	+100%
`keccak_f1600_x4_native_avx2`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`kem_enc`	✅	2s	3s	-33%
`kem_keypair_derand`	✅	2s	3s	-33%
`mlk_barrett_reduce`	✅	2s	1s	+100%
`mlk_check_pct`	✅	2s	2s	+0%
`mlk_ct_memcmp`	✅	2s	3s	-33%
`mlk_enc_getnoise_eta1_eta2`	✅	2s	1s	+100%
`mlk_gen_matrix`	✅	2s	3s	-33%
`mlk_keccakf1600_extract_bytes`	✅	2s	4s	-50%
`mlk_keccakf1600_xor_bytes`	✅	2s	1s	+100%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`mlk_keccakf1600x4_permute`	✅	2s	4s	-50%
`mlk_keypair_getnoise_eta1`	✅	2s	3s	-33%
`mlk_matvec_mul`	✅	2s	3s	-33%
`mlk_poly_compress_d11_c`	✅	2s	1s	+100%
`mlk_poly_compress_d11_native`	✅	2s	2s	+0%
`mlk_poly_compress_d5`	✅	2s	4s	-50%
`mlk_poly_compress_du`	✅	2s	1s	+100%
`mlk_poly_decompress_d10_c`	✅	2s	2s	+0%
`mlk_poly_decompress_d11`	✅	2s	2s	+0%
`mlk_poly_decompress_d11_c`	✅	2s	1s	+100%
`mlk_poly_decompress_d11_native`	✅	2s	2s	+0%
`mlk_poly_decompress_d4`	✅	2s	2s	+0%
`mlk_poly_decompress_d5`	✅	2s	2s	+0%
`mlk_poly_decompress_d5_c`	✅	2s	1s	+100%
`mlk_poly_decompress_du`	✅	2s	4s	-50%
`mlk_poly_frombytes`	✅	2s	2s	+0%
`mlk_poly_getnoise_eta1122_4x`	✅	2s	3s	-33%
`mlk_poly_getnoise_eta1_4x_native`	✅	2s	4s	-50%
`mlk_poly_invntt_tomont`	✅	2s	2s	+0%
`mlk_poly_invntt_tomont_c`	✅	2s	4s	-50%
`mlk_poly_mulcache_compute`	✅	2s	1s	+100%
`mlk_poly_reduce`	✅	2s	1s	+100%
`mlk_poly_sub`	✅	2s	1s	+100%
`mlk_poly_tobytes`	✅	2s	1s	+100%
`mlk_poly_tomsg`	✅	2s	3s	-33%
`mlk_polyvec_frombytes`	✅	2s	3s	-33%
`mlk_polyvec_invntt_tomont`	✅	2s	1s	+100%
`mlk_polyvec_reduce`	✅	2s	2s	+0%
`mlk_scalar_compress_d1`	✅	2s	3s	-33%
`mlk_scalar_compress_d10`	✅	2s	3s	-33%
`mlk_scalar_compress_d11`	✅	2s	3s	-33%
`mlk_scalar_decompress_d5`	✅	2s	3s	-33%
`mlk_scalar_signed_to_unsigned_q`	✅	2s	2s	+0%
`mlk_sha3_256`	✅	2s	3s	-33%
`mlk_sha3_512`	✅	2s	1s	+100%
`mlk_shake128_absorb_once`	✅	2s	1s	+100%
`mlk_shake128x4_squeezeblocks`	✅	2s	2s	+0%
`mlk_shake256`	✅	2s	1s	+100%
`mlk_value_barrier_u32`	✅	2s	4s	-50%
`mlk_value_barrier_u8`	✅	2s	1s	+100%
`poly_compress_d11_native_x86_64`	✅	2s	2s	+0%
`poly_compress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_decompress_d11_native_x86_64`	✅	2s	1s	+100%
`poly_decompress_d5_native_x86_64`	✅	2s	3s	-33%
`poly_getnoise_eta1122_4x_native`	✅	2s	1s	+100%
`poly_reduce_native_aarch64`	✅	2s	2s	+0%
`poly_tobytes_native_x86_64`	✅	2s	2s	+0%
`poly_tomont_native_aarch64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	3s	-33%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	1s	+100%
`intt_native_x86_64`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes_native`	✅	1s	6s	-83%
`mlk_ct_cmask_neg_i16`	✅	1s	2s	-50%
`mlk_ct_cmov_zero`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_i32`	✅	1s	3s	-67%
`mlk_ct_get_optblocker_u32`	✅	1s	1s	+0%
`mlk_ct_get_optblocker_u8`	✅	1s	3s	-67%
`mlk_ct_sel_uint8`	✅	1s	1s	+0%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	1s	3s	-67%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	1s	+0%
`mlk_keccakf1600x4_xor_bytes_c`	✅	1s	3s	-67%
`mlk_montgomery_reduce`	✅	1s	2s	-50%
`mlk_poly_add`	✅	1s	1s	+0%
`mlk_poly_compress_d4`	✅	1s	1s	+0%
`mlk_poly_compress_d4_native`	✅	1s	2s	-50%
`mlk_poly_compress_d5_native`	✅	1s	2s	-50%
`mlk_poly_decompress_d10`	✅	1s	3s	-67%
`mlk_poly_decompress_d4_c`	✅	1s	1s	+0%
`mlk_poly_frombytes_c`	✅	1s	2s	-50%
`mlk_poly_getnoise_eta2`	✅	1s	3s	-67%
`mlk_poly_tobytes_c`	✅	1s	3s	-67%
`mlk_poly_tobytes_native`	✅	1s	3s	-67%
`mlk_polyvec_compress_du`	✅	1s	2s	-50%
`mlk_polyvec_tobytes`	✅	1s	2s	-50%
`mlk_rej_uniform`	✅	1s	2s	-50%
`mlk_scalar_decompress_d4`	✅	1s	3s	-67%
`mlk_shake128_squeezeblocks`	✅	1s	2s	-50%
`mlk_value_barrier_i32`	✅	1s	2s	-50%
`ntt_native_x86_64`	✅	1s	2s	-50%
`poly_compress_d10_native_x86_64`	✅	1s	1s	+0%
`poly_compress_d4_native_x86_64`	✅	1s	4s	-75%
`poly_tomont_native_x86_64`	✅	1s	2s	-50%

oqs-bot · 2026-01-23T02:58:04Z

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1262s	1186s	+6.4%
`mlk_indcpa_enc`	✅	148s	139s	+6%
`mlk_rej_uniform_c`	✅	132s	121s	+9%
`mlk_indcpa_keypair_derand`	✅	131s	118s	+11%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	80s	81s	-1%
`polyvec_basemul_acc_montgomery_cached_native`	✅	36s	32s	+12%
`mlk_ntt_layer`	✅	35s	29s	+21%
`mlk_poly_rej_uniform`	✅	29s	26s	+12%
`mlk_keccak_squeezeblocks_x4`	✅	27s	26s	+4%
`poly_ntt_native`	✅	25s	23s	+9%
`mlk_poly_reduce_native`	✅	22s	20s	+10%
`mlk_fqmul`	✅	18s	16s	+12%
`keccakf1600x4_permute_native_x4`	✅	17s	18s	-6%
`mlk_poly_decompress_d5_native`	✅	16s	12s	+33%
`mlk_poly_decompress_d11_native`	✅	14s	14s	+0%
`mlk_indcpa_dec`	✅	11s	9s	+22%
`mlk_polyvec_add`	✅	11s	10s	+10%
`mlk_gen_matrix_serial`	✅	9s	4s	+125%
`mlk_keccak_squeeze_once`	✅	9s	8s	+12%
`mlk_poly_frombytes_native`	✅	9s	8s	+12%
`mlk_poly_frommsg`	✅	9s	10s	-10%
`mlk_poly_ntt`	✅	9s	5s	+80%
`mlk_ntt_butterfly_block`	✅	8s	7s	+14%
`kem_dec`	✅	7s	5s	+40%
`mlk_keccak_absorb_once_x4`	✅	7s	5s	+40%
`mlk_keccak_squeezeblocks`	✅	7s	8s	-12%
`mlk_poly_compress_d11_c`	✅	7s	5s	+40%
`rej_uniform_native_x86_64`	✅	7s	5s	+40%
`mlk_gen_matrix`	✅	6s	4s	+50%
`mlk_invntt_layer`	✅	6s	6s	+0%
`mlk_keccakf1600_permute_c`	✅	6s	8s	-25%
`mlk_poly_rej_uniform_x4`	✅	6s	6s	+0%
`mlk_polymat_permute_bitrev_to_custom`	✅	6s	6s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	5s	1s	+400%
`mlk_polyvec_decompress_du`	✅	5s	1s	+400%
`mlk_scalar_compress_d5`	✅	5s	3s	+67%
`poly_decompress_d5_native_x86_64`	✅	5s	3s	+67%
`poly_frombytes_native_x86_64`	✅	5s	5s	+0%
`rej_uniform_native`	✅	5s	2s	+150%
`kem_keypair_derand`	✅	4s	3s	+33%
`mlk_ct_cmov_zero`	✅	4s	1s	+300%
`mlk_keccakf1600x4_extract_bytes_c`	✅	4s	1s	+300%
`mlk_matvec_mul`	✅	4s	5s	-20%
`mlk_poly_compress_d11`	✅	4s	3s	+33%
`mlk_poly_compress_d4_native`	✅	4s	3s	+33%
`mlk_poly_compress_d5`	✅	4s	2s	+100%
`mlk_poly_decompress_d10_native`	✅	4s	4s	+0%
`mlk_poly_getnoise_eta2`	✅	4s	2s	+100%
`mlk_polyvec_frombytes`	✅	4s	2s	+100%
`poly_compress_d4_native_x86_64`	✅	4s	1s	+300%
`poly_decompress_d11_native_x86_64`	✅	4s	4s	+0%
`poly_decompress_d4_native_x86_64`	✅	4s	3s	+33%
`poly_mulcache_compute_native_x86_64`	✅	4s	4s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	4s	3s	+33%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	4s	2s	+100%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	1s	+200%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes_native`	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes_native`	✅	3s	2s	+50%
`kem_check_sk`	✅	3s	4s	-25%
`kem_enc`	✅	3s	3s	+0%
`kem_keypair`	✅	3s	4s	-25%
`mlk_check_pct`	✅	3s	2s	+50%
`mlk_ct_cmask_neg_i16`	✅	3s	2s	+50%
`mlk_ct_sel_uint8`	✅	3s	2s	+50%
`mlk_enc_getnoise_eta1_eta2`	✅	3s	1s	+200%
`mlk_keccak_absorb_once`	✅	3s	3s	+0%
`mlk_keccakf1600_xor_bytes`	✅	3s	2s	+50%
`mlk_keccakf1600x4_extract_bytes`	✅	3s	4s	-25%
`mlk_keccakf1600x4_permute`	✅	3s	1s	+200%
`mlk_montgomery_reduce`	✅	3s	4s	-25%
`mlk_poly_add`	✅	3s	2s	+50%
`mlk_poly_cbd_eta2`	✅	3s	3s	+0%
`mlk_poly_compress_d10_native`	✅	3s	1s	+200%
`mlk_poly_compress_d11_native`	✅	3s	3s	+0%
`mlk_poly_compress_d5_c`	✅	3s	1s	+200%
`mlk_poly_compress_du`	✅	3s	1s	+200%
`mlk_poly_decompress_d10`	✅	3s	3s	+0%
`mlk_poly_decompress_d4_c`	✅	3s	2s	+50%
`mlk_poly_frombytes`	✅	3s	4s	-25%
`mlk_poly_getnoise_eta1122_4x`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x`	✅	3s	4s	-25%
`mlk_poly_getnoise_eta1_4x_native`	✅	3s	3s	+0%
`mlk_poly_mulcache_compute_c`	✅	3s	3s	+0%
`mlk_poly_ntt_c`	✅	3s	2s	+50%
`mlk_poly_tobytes`	✅	3s	2s	+50%
`mlk_poly_tobytes_native`	✅	3s	3s	+0%
`mlk_poly_tomsg`	✅	3s	2s	+50%
`mlk_polyvec_mulcache_compute`	✅	3s	3s	+0%
`mlk_scalar_compress_d10`	✅	3s	2s	+50%
`mlk_scalar_compress_d11`	✅	3s	2s	+50%
`mlk_scalar_decompress_d10`	✅	3s	2s	+50%
`mlk_scalar_signed_to_unsigned_q`	✅	3s	2s	+50%
`mlk_shake128_squeezeblocks`	✅	3s	4s	-25%
`mlk_shake128x4_squeezeblocks`	✅	3s	3s	+0%
`mlk_shake256x4`	✅	3s	5s	-40%
`ntt_native_aarch64`	✅	3s	2s	+50%
`ntt_native_x86_64`	✅	3s	3s	+0%
`poly_compress_d10_native_x86_64`	✅	3s	1s	+200%
`poly_compress_d11_native_x86_64`	✅	3s	5s	-40%
`poly_getnoise_eta1122_4x_native`	✅	3s	2s	+50%
`poly_mulcache_compute_native_aarch64`	✅	3s	2s	+50%
`poly_reduce_native_x86_64`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	2s	4s	-50%
`intt_native_x86_64`	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`kem_check_pk`	✅	2s	5s	-60%
`kem_enc_derand`	✅	2s	4s	-50%
`mlk_barrett_reduce`	✅	2s	3s	-33%
`mlk_ct_get_optblocker_u32`	✅	2s	2s	+0%
`mlk_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mlk_ct_memcmp`	✅	2s	2s	+0%
`mlk_ct_sel_int16`	✅	2s	1s	+100%
`mlk_keccakf1600_extract_bytes`	✅	2s	1s	+100%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`mlk_keccakf1600_permute`	✅	2s	1s	+100%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	2s	3s	-33%
`mlk_keccakf1600x4_xor_bytes_c`	✅	2s	1s	+100%
`mlk_poly_cbd_eta1`	✅	2s	4s	-50%
`mlk_poly_compress_d10`	✅	2s	2s	+0%
`mlk_poly_compress_d10_c`	✅	2s	4s	-50%
`mlk_poly_compress_d4`	✅	2s	1s	+100%
`mlk_poly_compress_d4_c`	✅	2s	2s	+0%
`mlk_poly_compress_d5_native`	✅	2s	3s	-33%
`mlk_poly_decompress_d4`	✅	2s	1s	+100%
`mlk_poly_decompress_d4_native`	✅	2s	2s	+0%
`mlk_poly_decompress_d5`	✅	2s	4s	-50%
`mlk_poly_decompress_d5_c`	✅	2s	4s	-50%
`mlk_poly_decompress_du`	✅	2s	3s	-33%
`mlk_poly_decompress_dv`	✅	2s	2s	+0%
`mlk_poly_invntt_tomont`	✅	2s	4s	-50%
`mlk_poly_mulcache_compute_native`	✅	2s	3s	-33%
`mlk_poly_reduce_c`	✅	2s	1s	+100%
`mlk_poly_sub`	✅	2s	2s	+0%
`mlk_poly_tomont`	✅	2s	4s	-50%
`mlk_poly_tomont_native`	✅	2s	1s	+100%
`mlk_polyvec_compress_du`	✅	2s	2s	+0%
`mlk_polyvec_invntt_tomont`	✅	2s	2s	+0%
`mlk_polyvec_ntt`	✅	2s	3s	-33%
`mlk_polyvec_permute_bitrev_to_custom`	✅	2s	2s	+0%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	2s	2s	+0%
`mlk_polyvec_reduce`	✅	2s	3s	-33%
`mlk_polyvec_tomont`	✅	2s	4s	-50%
`mlk_rej_uniform`	✅	2s	3s	-33%
`mlk_scalar_compress_d1`	✅	2s	2s	+0%
`mlk_scalar_decompress_d11`	✅	2s	2s	+0%
`mlk_scalar_decompress_d4`	✅	2s	2s	+0%
`mlk_sha3_256`	✅	2s	1s	+100%
`mlk_sha3_512`	✅	2s	1s	+100%
`mlk_shake128_absorb_once`	✅	2s	2s	+0%
`mlk_shake256`	✅	2s	2s	+0%
`mlk_value_barrier_i32`	✅	2s	5s	-60%
`mlk_value_barrier_u8`	✅	2s	3s	-33%
`nttunpack_native_x86_64`	✅	2s	6s	-67%
`poly_compress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_decompress_d10_native_x86_64`	✅	2s	1s	+100%
`poly_invntt_tomont_native`	✅	2s	3s	-33%
`poly_reduce_native_aarch64`	✅	2s	3s	-33%
`poly_tobytes_native_x86_64`	✅	2s	1s	+100%
`poly_tomont_native_aarch64`	✅	2s	2s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native_aarch64`	✅	2s	3s	-33%
`sys_check_capability`	✅	2s	1s	+100%
`keccak_f1600_x1_native_aarch64`	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	2s	-50%
`keccakf1600_permute_native`	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u16`	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u8`	✅	1s	2s	-50%
`mlk_ct_get_optblocker_i32`	✅	1s	1s	+0%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	1s	+0%
`mlk_keypair_getnoise_eta1`	✅	1s	4s	-75%
`mlk_poly_compress_dv`	✅	1s	3s	-67%
`mlk_poly_decompress_d10_c`	✅	1s	4s	-75%
`mlk_poly_decompress_d11`	✅	1s	2s	-50%
`mlk_poly_decompress_d11_c`	✅	1s	1s	+0%
`mlk_poly_frombytes_c`	✅	1s	3s	-67%
`mlk_poly_invntt_tomont_c`	✅	1s	3s	-67%
`mlk_poly_mulcache_compute`	✅	1s	2s	-50%
`mlk_poly_reduce`	✅	1s	1s	+0%
`mlk_poly_tobytes_c`	✅	1s	2s	-50%
`mlk_poly_tomont_c`	✅	1s	2s	-50%
`mlk_polyvec_tobytes`	✅	1s	3s	-67%
`mlk_scalar_compress_d4`	✅	1s	3s	-67%
`mlk_scalar_decompress_d5`	✅	1s	1s	+0%
`mlk_shake128x4_absorb_once`	✅	1s	2s	-50%
`mlk_value_barrier_u32`	✅	1s	2s	-50%
`poly_tobytes_native_aarch64`	✅	1s	4s	-75%
`poly_tomont_native_x86_64`	✅	1s	2s	-50%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	1s	4s	-75%

oqs-bot · 2026-01-23T03:00:58Z

CBMC Results (ML-KEM-768)

Full Results (191 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1230s	1229s	+0.1%
`mlk_indcpa_keypair_derand`	✅	191s	189s	+1%
`mlk_indcpa_enc`	✅	164s	169s	-3%
`mlk_rej_uniform_c`	✅	122s	109s	+12%
`mlk_polyvec_basemul_acc_montgomery_cached_c`	✅	43s	44s	-2%
`mlk_poly_rej_uniform`	✅	30s	31s	-3%
`poly_ntt_native`	✅	28s	25s	+12%
`mlk_ntt_layer`	✅	27s	32s	-16%
`mlk_keccak_squeezeblocks_x4`	✅	25s	25s	+0%
`mlk_poly_reduce_native`	✅	20s	20s	+0%
`polyvec_basemul_acc_montgomery_cached_native`	✅	20s	16s	+25%
`keccakf1600x4_permute_native_x4`	✅	18s	19s	-5%
`mlk_fqmul`	✅	17s	16s	+6%
`mlk_poly_decompress_d4_native`	✅	16s	15s	+7%
`mlk_indcpa_dec`	✅	14s	12s	+17%
`mlk_poly_decompress_d10_native`	✅	12s	16s	-25%
`mlk_polyvec_add`	✅	11s	10s	+10%
`mlk_keccak_squeezeblocks`	✅	10s	8s	+25%
`mlk_ntt_butterfly_block`	✅	8s	6s	+33%
`mlk_poly_frombytes_native`	✅	8s	7s	+14%
`mlk_keccak_squeeze_once`	✅	7s	8s	-12%
`mlk_poly_frommsg`	✅	7s	8s	-12%
`kem_dec`	✅	6s	5s	+20%
`mlk_keccak_absorb_once_x4`	✅	6s	6s	+0%
`mlk_keccakf1600_permute_c`	✅	6s	6s	+0%
`mlk_poly_add`	✅	6s	2s	+200%
`mlk_poly_rej_uniform_x4`	✅	6s	6s	+0%
`rej_uniform_native_x86_64`	✅	6s	5s	+20%
`mlk_gen_matrix`	✅	5s	2s	+150%
`mlk_poly_ntt`	✅	5s	6s	-17%
`mlk_poly_ntt_c`	✅	5s	3s	+67%
`poly_decompress_d4_native_x86_64`	✅	5s	4s	+25%
`mlk_barrett_reduce`	✅	4s	2s	+100%
`mlk_invntt_layer`	✅	4s	4s	+0%
`mlk_keccak_absorb_once`	✅	4s	4s	+0%
`mlk_keccakf1600_permute`	✅	4s	2s	+100%
`mlk_poly_compress_d5_c`	✅	4s	3s	+33%
`mlk_poly_decompress_d10_c`	✅	4s	4s	+0%
`mlk_poly_decompress_d5_native`	✅	4s	3s	+33%
`mlk_poly_reduce_c`	✅	4s	2s	+100%
`mlk_polymat_permute_bitrev_to_custom`	✅	4s	5s	-20%
`mlk_polyvec_tobytes`	✅	4s	3s	+33%
`mlk_scalar_decompress_d10`	✅	4s	2s	+100%
`mlk_scalar_signed_to_unsigned_q`	✅	4s	3s	+33%
`mlk_sha3_256`	✅	4s	3s	+33%
`mlk_shake128_absorb_once`	✅	4s	5s	-20%
`nttunpack_native_x86_64`	✅	4s	4s	+0%
`poly_decompress_d10_native_x86_64`	✅	4s	4s	+0%
`poly_decompress_d11_native_x86_64`	✅	4s	2s	+100%
`poly_frombytes_native_x86_64`	✅	4s	3s	+33%
`poly_tobytes_native_aarch64`	✅	4s	4s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_aarch64`	✅	4s	3s	+33%
`polyvec_basemul_acc_montgomery_cached_k3_native_aarch64`	✅	4s	3s	+33%
`intt_native_x86_64`	✅	3s	1s	+200%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	2s	+50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	3s	2s	+50%
`keccakf1600x4_xor_bytes_native`	✅	3s	7s	-57%
`kem_enc`	✅	3s	1s	+200%
`kem_keypair`	✅	3s	2s	+50%
`mlk_check_pct`	✅	3s	3s	+0%
`mlk_ct_cmask_nonzero_u16`	✅	3s	2s	+50%
`mlk_ct_get_optblocker_i32`	✅	3s	1s	+200%
`mlk_ct_get_optblocker_u8`	✅	3s	2s	+50%
`mlk_ct_memcmp`	✅	3s	4s	-25%
`mlk_enc_getnoise_eta1_eta2`	✅	3s	2s	+50%
`mlk_keccakf1600_extract_bytes`	✅	3s	1s	+200%
`mlk_keccakf1600_xor_bytes`	✅	3s	1s	+200%
`mlk_keccakf1600x4_xor_bytes_c`	✅	3s	2s	+50%
`mlk_matvec_mul`	✅	3s	2s	+50%
`mlk_montgomery_reduce`	✅	3s	3s	+0%
`mlk_poly_cbd_eta1`	✅	3s	3s	+0%
`mlk_poly_compress_d11`	✅	3s	3s	+0%
`mlk_poly_compress_d4_c`	✅	3s	2s	+50%
`mlk_poly_compress_dv`	✅	3s	2s	+50%
`mlk_poly_decompress_d10`	✅	3s	2s	+50%
`mlk_poly_getnoise_eta1_4x`	✅	3s	6s	-50%
`mlk_poly_mulcache_compute`	✅	3s	3s	+0%
`mlk_poly_mulcache_compute_c`	✅	3s	3s	+0%
`mlk_poly_tobytes`	✅	3s	2s	+50%
`mlk_polyvec_decompress_du`	✅	3s	2s	+50%
`mlk_polyvec_frombytes`	✅	3s	3s	+0%
`mlk_polyvec_invntt_tomont`	✅	3s	2s	+50%
`mlk_polyvec_permute_bitrev_to_custom_native`	✅	3s	4s	-25%
`mlk_rej_uniform`	✅	3s	3s	+0%
`mlk_scalar_decompress_d11`	✅	3s	1s	+200%
`mlk_shake128x4_squeezeblocks`	✅	3s	2s	+50%
`mlk_shake256`	✅	3s	3s	+0%
`mlk_shake256x4`	✅	3s	2s	+50%
`mlk_value_barrier_i32`	✅	3s	2s	+50%
`ntt_native_aarch64`	✅	3s	2s	+50%
`poly_compress_d10_native_x86_64`	✅	3s	1s	+200%
`poly_compress_d11_native_x86_64`	✅	3s	1s	+200%
`poly_compress_d4_native_x86_64`	✅	3s	4s	-25%
`poly_compress_d5_native_x86_64`	✅	3s	2s	+50%
`poly_mulcache_compute_native_aarch64`	✅	3s	1s	+200%
`poly_reduce_native_aarch64`	✅	3s	3s	+0%
`polyvec_basemul_acc_montgomery_cached_k2_native_x86_64`	✅	3s	4s	-25%
`polyvec_basemul_acc_montgomery_cached_k4_native_x86_64`	✅	3s	3s	+0%
`rej_uniform_native_aarch64`	✅	3s	5s	-40%
`intt_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccakf1600x4_extract_bytes_native`	✅	2s	3s	-33%
`kem_enc_derand`	✅	2s	1s	+100%
`kem_keypair_derand`	✅	2s	4s	-50%
`mlk_ct_cmask_neg_i16`	✅	2s	3s	-33%
`mlk_ct_get_optblocker_u32`	✅	2s	4s	-50%
`mlk_ct_sel_int16`	✅	2s	3s	-33%
`mlk_ct_sel_uint8`	✅	2s	4s	-50%
`mlk_gen_matrix_serial`	✅	2s	3s	-33%
`mlk_keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`mlk_keccakf1600_xor_bytes (big endian)`	✅	2s	3s	-33%
`mlk_keccakf1600x4_extract_bytes`	✅	2s	3s	-33%
`mlk_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mlk_keccakf1600x4_permute`	✅	2s	1s	+100%
`mlk_keypair_getnoise_eta1`	✅	2s	3s	-33%
`mlk_poly_compress_d10`	✅	2s	1s	+100%
`mlk_poly_compress_d10_c`	✅	2s	5s	-60%
`mlk_poly_compress_d10_native`	✅	2s	1s	+100%
`mlk_poly_compress_d4`	✅	2s	2s	+0%
`mlk_poly_compress_d4_native`	✅	2s	3s	-33%
`mlk_poly_compress_d5`	✅	2s	3s	-33%
`mlk_poly_decompress_d11`	✅	2s	2s	+0%
`mlk_poly_decompress_d4_c`	✅	2s	1s	+100%
`mlk_poly_decompress_d5`	✅	2s	3s	-33%
`mlk_poly_decompress_du`	✅	2s	1s	+100%
`mlk_poly_decompress_dv`	✅	2s	3s	-33%
`mlk_poly_frombytes`	✅	2s	1s	+100%
`mlk_poly_getnoise_eta1122_4x`	✅	2s	2s	+0%
`mlk_poly_getnoise_eta2`	✅	2s	1s	+100%
`mlk_poly_invntt_tomont`	✅	2s	3s	-33%
`mlk_poly_mulcache_compute_native`	✅	2s	2s	+0%
`mlk_poly_reduce`	✅	2s	3s	-33%
`mlk_poly_sub`	✅	2s	2s	+0%
`mlk_poly_tobytes_c`	✅	2s	1s	+100%
`mlk_poly_tobytes_native`	✅	2s	4s	-50%
`mlk_poly_tomont_c`	✅	2s	2s	+0%
`mlk_poly_tomont_native`	✅	2s	3s	-33%
`mlk_poly_tomsg`	✅	2s	2s	+0%
`mlk_polyvec_basemul_acc_montgomery_cached`	✅	2s	1s	+100%
`mlk_polyvec_compress_du`	✅	2s	1s	+100%
`mlk_polyvec_mulcache_compute`	✅	2s	4s	-50%
`mlk_polyvec_ntt`	✅	2s	2s	+0%
`mlk_polyvec_permute_bitrev_to_custom`	✅	2s	3s	-33%
`mlk_polyvec_reduce`	✅	2s	4s	-50%
`mlk_scalar_compress_d1`	✅	2s	2s	+0%
`mlk_scalar_compress_d10`	✅	2s	2s	+0%
`mlk_scalar_compress_d11`	✅	2s	1s	+100%
`mlk_scalar_decompress_d4`	✅	2s	2s	+0%
`mlk_scalar_decompress_d5`	✅	2s	2s	+0%
`mlk_sha3_512`	✅	2s	2s	+0%
`mlk_value_barrier_u32`	✅	2s	2s	+0%
`poly_decompress_d5_native_x86_64`	✅	2s	2s	+0%
`poly_getnoise_eta1122_4x_native`	✅	2s	1s	+100%
`poly_invntt_tomont_native`	✅	2s	3s	-33%
`poly_reduce_native_x86_64`	✅	2s	3s	-33%
`poly_tobytes_native_x86_64`	✅	2s	2s	+0%
`poly_tomont_native_x86_64`	✅	2s	1s	+100%
`polyvec_basemul_acc_montgomery_cached_k3_native_x86_64`	✅	2s	4s	-50%
`polyvec_basemul_acc_montgomery_cached_k4_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	1s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	1s	+0%
`keccak_f1600_x4_native_avx2`	✅	1s	1s	+0%
`keccakf1600_permute_native`	✅	1s	3s	-67%
`kem_check_pk`	✅	1s	3s	-67%
`kem_check_sk`	✅	1s	2s	-50%
`mlk_ct_cmask_nonzero_u8`	✅	1s	2s	-50%
`mlk_ct_cmov_zero`	✅	1s	3s	-67%
`mlk_keccakf1600x4_xor_bytes`	✅	1s	5s	-80%
`mlk_poly_cbd_eta2`	✅	1s	2s	-50%
`mlk_poly_compress_d11_c`	✅	1s	2s	-50%
`mlk_poly_compress_d11_native`	✅	1s	2s	-50%
`mlk_poly_compress_d5_native`	✅	1s	2s	-50%
`mlk_poly_compress_du`	✅	1s	4s	-75%
`mlk_poly_decompress_d11_c`	✅	1s	2s	-50%
`mlk_poly_decompress_d11_native`	✅	1s	3s	-67%
`mlk_poly_decompress_d4`	✅	1s	1s	+0%
`mlk_poly_decompress_d5_c`	✅	1s	2s	-50%
`mlk_poly_frombytes_c`	✅	1s	3s	-67%
`mlk_poly_getnoise_eta1_4x_native`	✅	1s	2s	-50%
`mlk_poly_invntt_tomont_c`	✅	1s	3s	-67%
`mlk_poly_tomont`	✅	1s	2s	-50%
`mlk_polyvec_tomont`	✅	1s	2s	-50%
`mlk_scalar_compress_d4`	✅	1s	2s	-50%
`mlk_scalar_compress_d5`	✅	1s	2s	-50%
`mlk_shake128_squeezeblocks`	✅	1s	1s	+0%
`mlk_shake128x4_absorb_once`	✅	1s	2s	-50%
`mlk_value_barrier_u8`	✅	1s	3s	-67%
`ntt_native_x86_64`	✅	1s	2s	-50%
`poly_mulcache_compute_native_x86_64`	✅	1s	3s	-67%
`poly_tomont_native_aarch64`	✅	1s	3s	-67%
`sys_check_capability`	✅	1s	2s	-50%

hanno-becker · 2026-03-19T05:11:10Z

@willieyz Could you rebase this please?

willieyz · 2026-03-21T04:03:25Z

@willieyz Could you rebase this please?

Hello @hanno-becker,
sorry for the late reply...
I’m on vacation right now and will be back on March 23. Is it okay if I rebase the PR then?
I will report with discord chat when I finish the rebase!

willieyz · 2026-03-25T02:48:52Z

Hello, @hanno-becker ,
I had rebase this on top of main. Could you please take another look when you have time?
Thank you for you help!

mkannwischer

Thanks @willieyz. Generally I support this change for consistency and I checked that you have not missed any non-namespaced macros.

A couple of comments got wrongly changed in the x86_64 code (see below), please change them back.

Since the scope of this PR has changed, please update the commit message and PR description to reflect that.

mkannwischer · 2026-04-04T02:16:59Z

 //
 //  Notes:
-//    - We exit early if we find the required number of good values,
+//    - We exit early if we find the required number of MLK_GOOD values,


Suggested change

// - We exit early if we find the required number of MLK_GOOD values,

// - We exit early if we find the required number of good values,

mkannwischer · 2026-04-04T02:17:08Z

+//       occupies a corresponding 16-bit element of `MLK_VALS` xmm register,
+//    2. Compute an 8-bit value `MLK_GOOD` such that
+//         MLK_GOOD[i] = MLK_VALS[i] < MLKEM_Q ? 1 : 0, for i in [0, 7],
+//    3. Shuffle the elements in `MLK_VALS` such that all MLK_GOOD elements


Suggested change

// 3. Shuffle the elements in `MLK_VALS` such that all MLK_GOOD elements

// 3. Shuffle the elements in `MLK_VALS` such that all good elements

mkannwischer · 2026-04-04T02:17:37Z

-  movq $0, cnt // cnt counts the number of good values we've found.
-  movq $0, pos // pos is the current position in the input buffer.
-  movq $0x5555, pext_mask // 0x5555 mask to extract every second bit.
+  movq $0, MLK_CNT // MLK_CNT counts the number of MLK_GOOD values we've found.


Suggested change

movq $0, MLK_CNT // MLK_CNT counts the number of MLK_GOOD values we've found.

movq $0, MLK_CNT // MLK_CNT counts the number of good values we've found.

mkannwischer · 2026-04-04T02:18:21Z

+  pinsrq $1, %rax, MLK_BOUND

-  // Broadcast 12-bit mask 0xFFF to all 16-bit elements of bound reg.
+  // Broadcast 12-bit mask 0xFFF to all 16-bit elements of MLK_BOUND reg.


Suggested change

// Broadcast 12-bit mask 0xFFF to all 16-bit elements of MLK_BOUND reg.

// Broadcast 12-bit mask 0xFFF to all 16-bit elements of MLK_AND_MASK reg.

mkannwischer · 2026-04-04T02:21:07Z

Marking as draft for now. Please mark it as ready when my comments have been addressed.

mkannwischer · 2026-04-12T15:45:22Z

@willieyz - gentle ping. Could you please get this updated so we can get it merged?

willieyz · 2026-04-13T09:04:02Z

@willieyz - gentle ping. Could you please get this updated so we can get it merged?

Hello @mkannwischer,
Sorry for the long period of inactivity due to other work recently. I’m now back to my normal work routine and have addressed the changes you suggested.
Could you please take another look, I will fix ASAP if there is any problem.
Thank you again for your review.

mkannwischer

None of my previous comments are addressed. Please fix.

willieyz · 2026-04-23T03:51:41Z

None of my previous comments are addressed. Please fix.

Hello, @mkannwischer ,
Sorry for the confusion earlier. I didn’t realize that I hadn’t pushed after changing...,
I’ve made sure everything is pushed now, and also revise the commit message and PR description.

Apologies for the extra review effort, and thank you for your patience, could you please kindly take another look when you have time?
Thank you for your help.

mkannwischer · 2026-04-23T03:53:56Z

None of my previous comments are addressed. Please fix.

Hello, @mkannwischer , Sorry for the confusion earlier. I didn’t realize that I hadn’t pushed after changing..., I’ve made sure everything is pushed now, and also revise the commit message and PR description.

Apologies for the extra review effort, and thank you for your patience, could you please kindly take another look when you have time? Thank you for your help.

While you are at it, can you change to the most recent SLOTHY version (0.2.0)? You should be able to just use the version not the commit.

- Assembly files may define local macros (e.g. `STACK_SIZE`, `KECCAK_F1600_ROUNDS`) without the `MLK_` prefix, risking name clashes with symbols in consuming libraries. - To be consistent with the rest of the codebase, all such macros are prefixed with `MLK_`, bringing them in line with the established namespacing convention. Signed-off-by: willieyz <willie.zhao@chelpis.com>

mkannwischer · 2026-04-25T04:56:43Z

After discussing with @hanno-becker, we have concluded that the loss in readability in rej_uniform_avx2_asm.S is not worth it given that the simplified assemly in mlkem/ doesn't contain the non-namespaced macros anyway.
Thank you @willieyz for looking into this and adding the required support to SLOTHY - I'm sure that will be useful elsewhere.

willieyz marked this pull request as ready for review December 17, 2025 02:28

willieyz requested a review from a team as a code owner December 17, 2025 02:28

hanno-becker reviewed Dec 17, 2025

View reviewed changes

hanno-becker requested changes Dec 17, 2025

View reviewed changes

willieyz force-pushed the namespace-STACK_SIZE branch 3 times, most recently from a7001df to 59a18fd Compare December 17, 2025 10:50

willieyz marked this pull request as draft December 18, 2025 02:00

willieyz force-pushed the namespace-STACK_SIZE branch 2 times, most recently from e96e223 to 0878495 Compare December 31, 2025 10:24

willieyz marked this pull request as ready for review December 31, 2025 10:39

willieyz marked this pull request as draft December 31, 2025 11:06

willieyz force-pushed the namespace-STACK_SIZE branch 4 times, most recently from f855045 to b6a4787 Compare January 3, 2026 20:24

willieyz mentioned this pull request Jan 5, 2026

Make naming of stack locations configurable slothy-optimizer/slothy#386

Merged

willieyz force-pushed the namespace-STACK_SIZE branch 2 times, most recently from 4db09cb to 5f64f67 Compare January 12, 2026 03:46

willieyz requested a review from hanno-becker January 22, 2026 02:27

willieyz marked this pull request as ready for review January 22, 2026 02:27

willieyz marked this pull request as draft January 23, 2026 02:29

willieyz force-pushed the namespace-STACK_SIZE branch from 0b7e708 to 17d96d2 Compare January 23, 2026 02:35

willieyz force-pushed the namespace-STACK_SIZE branch from 17d96d2 to 4be4259 Compare January 23, 2026 06:19

willieyz marked this pull request as ready for review January 23, 2026 10:05

willieyz marked this pull request as draft January 23, 2026 10:12

willieyz marked this pull request as ready for review January 23, 2026 11:00

willieyz force-pushed the namespace-STACK_SIZE branch from 4be4259 to 68eabf4 Compare March 23, 2026 17:11

mkannwischer self-assigned this Apr 2, 2026

mkannwischer added the needs-mldsa-native-port label Apr 4, 2026

mkannwischer requested changes Apr 4, 2026

View reviewed changes

mkannwischer marked this pull request as draft April 4, 2026 02:21

willieyz force-pushed the namespace-STACK_SIZE branch from 68eabf4 to bddb1d2 Compare April 13, 2026 03:12

willieyz marked this pull request as ready for review April 13, 2026 09:04

willieyz requested a review from mkannwischer April 13, 2026 09:05

willieyz force-pushed the namespace-STACK_SIZE branch from bddb1d2 to bee554b Compare April 16, 2026 16:37

mkannwischer force-pushed the namespace-STACK_SIZE branch from bee554b to 0110138 Compare April 22, 2026 03:23

mkannwischer requested changes Apr 22, 2026

View reviewed changes

willieyz force-pushed the namespace-STACK_SIZE branch 2 times, most recently from 8558864 to d5bf6d3 Compare April 23, 2026 03:40

willieyz force-pushed the namespace-STACK_SIZE branch 2 times, most recently from 0920843 to c68e02e Compare April 23, 2026 07:57

mkannwischer force-pushed the namespace-STACK_SIZE branch from c68e02e to 88208ec Compare April 25, 2026 04:25

mkannwischer closed this Apr 25, 2026

mkannwischer mentioned this pull request Apr 25, 2026

Namespace STACK_SIZE in various assembly files #1395

Closed

	// - We exit early if we find the required number of MLK_GOOD values,
	// - We exit early if we find the required number of good values,

	// 3. Shuffle the elements in `MLK_VALS` such that all MLK_GOOD elements
	// 3. Shuffle the elements in `MLK_VALS` such that all good elements

	movq $0, MLK_CNT // MLK_CNT counts the number of MLK_GOOD values we've found.
	movq $0, MLK_CNT // MLK_CNT counts the number of good values we've found.

	// Broadcast 12-bit mask 0xFFF to all 16-bit elements of MLK_BOUND reg.
	// Broadcast 12-bit mask 0xFFF to all 16-bit elements of MLK_AND_MASK reg.

Conversation

willieyz commented Dec 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

oqs-bot commented Jan 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-512)

Uh oh!

oqs-bot commented Jan 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

oqs-bot commented Jan 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-768)

Uh oh!

hanno-becker commented Mar 19, 2026

Uh oh!

willieyz commented Mar 21, 2026

Uh oh!

willieyz commented Mar 25, 2026

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mkannwischer commented Apr 4, 2026

Uh oh!

mkannwischer commented Apr 12, 2026

Uh oh!

willieyz commented Apr 13, 2026

Uh oh!

mkannwischer left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

willieyz commented Apr 23, 2026

Uh oh!

mkannwischer commented Apr 23, 2026

Uh oh!

mkannwischer commented Apr 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

willieyz commented Dec 16, 2025 •

edited

Loading

oqs-bot commented Jan 23, 2026 •

edited

Loading

oqs-bot commented Jan 23, 2026 •

edited

Loading

oqs-bot commented Jan 23, 2026 •

edited

Loading

mkannwischer left a comment •

edited

Loading